Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi

摘要

In this paper we consider propositional calculi, which are finitelyaxiomatizable extensions of intuitionistic implicational propositional calculustogether with the rules of modus ponens and substitution. We give a proof ofundecidability of the following problem for these calculi: whether a givenfinite set of propositional formulas constitutes an adequate axiom system for afixed propositional calculus. Moreover, we prove the same for the followingrestriction of this problem: whether a given finite set of theorems of a fixedpropositional calculus derives all theorems of this calculus. The proof ofthese results is based on a reduction of the undecidable halting problem forthe tag systems introduced by Post.